Skip to content

Add minimal browser UI and update prover documentation#100

Merged
hyperpolymath merged 7 commits into
mainfrom
claude/determined-archimedes-Sgffi
May 24, 2026
Merged

Add minimal browser UI and update prover documentation#100
hyperpolymath merged 7 commits into
mainfrom
claude/determined-archimedes-Sgffi

Conversation

@hyperpolymath

@hyperpolymath hyperpolymath commented May 23, 2026

Copy link
Copy Markdown
Owner

Summary

This PR introduces a self-contained browser UI for proof submission and updates documentation to reflect the actual prover surface exposed by the REST API. The changes clarify that while ECHIDNA implements 100+ prover backends, the default API surface is deliberately limited to a 12-prover core set.

Key Changes

  • New file: src/ui/public/prove.html — A minimal, self-contained REST client UI for proof submission

    • No build step required; opens directly in any modern browser via file://
    • Connects to a running ECHIDNA server (e.g., cargo run -- server --cors)
    • Supports prover selection, timeout configuration, neural assist toggle
    • Displays proof results with elapsed time, goal count, and outcome status
    • Includes example SMT-LIB snippets (Z3 SAT/UNSAT) for quick testing
    • Dark theme with GitHub-inspired color palette

  • New file: docs/SUPPORTED_PROVERS.md — Authoritative documentation of prover support

    • Clarifies the 12-prover core set exposed via GET /api/provers
    • Documents required external binaries and installation hints for each core prover
    • Explains the distinction between core (12), advertised (67), and total (141) prover variants
    • Provides quickstart instructions for proving the first goal with Z3
    • Describes how to expose additional backends through the REST API

  • Updated: README.adoc

    • Revised prover badge from "128" to "12 core / 67 advertised"
    • Updated test count from "917+" to "1059"
    • Replaced "Leadership Position" section with "Prover Surface" and "Distinguishing Features"
    • Simplified prover tier table to focus on the 12-core set
    • Added "Prove your first goal" quickstart section with curl examples
    • Updated architecture documentation to reflect 102 backend implementation files
    • Clarified test suite counts and VeriSim integration

  • Minor: src/rust/corpus/octad.rs — Refactored hex formatting

    • Extracted to_hex() helper function to avoid repeated format!("{:x}", ...) patterns
    • Applied consistently across octad_key(), cross_prover_key(), content_hash_of(), and hash_provenance()
    • Improves code maintainability and readability

Implementation Details

The browser UI (prove.html) is fully self-contained with:

  • Inline CSS (dark theme with semantic color variables)
  • Vanilla JavaScript (no dependencies)
  • Health check polling on API base change
  • Prover roster auto-loading from /api/provers
  • Real-time result display with outcome classification (ok/bad/warn)
  • Example snippets that auto-populate content and prover selection

The documentation updates align the public-facing narrative with the actual REST API surface, reducing confusion for new users while preserving the full 100+ prover capability for Rust API consumers.

https://claude.ai/code/session_01RLu1DN3tSHfaVc8aqTd7VZ

claude added 2 commits May 23, 2026 19:38
@claude
fix(corpus): replace LowerHex format with manual hex encoding
319cc49 
sha2's newer digest::Output (Array<u8, N>) drops LowerHex, so the four
`format!("{:x}", h.finalize())` sites in src/rust/corpus/octad.rs no
longer compile. Add a local zero-dep `to_hex` helper and use it at all
four sites. Unblocks `cargo build` on fresh clone.

feat(ui): add minimal self-contained REST client at src/ui/public/prove.html

Single static page (vanilla JS + inline CSS, Tailwind-free) that drives
the existing /api/health, /api/provers, /api/prove, and /api/verify
endpoints. Open directly in a browser and point at a server started
with `echidna server --cors`. Independent of the in-progress
AffineScript-TEA migration so it doesn't disturb that work.
@claude
docs: correct prover/test counts and add SUPPORTED_PROVERS.md
672c153 
The README advertised "128 provers / 917+ tests". Ground truth:

  - ProverKind enum: 141 variants
  - src/rust/provers/*.rs implementation files: 102
  - ProverKind::all() (advertised roster): 67
  - ProverKind::all_core() (REST API surface): 12
  - cargo test --lib on default features: 1059 passing, 2 ignored

Replace the inflated 128/917 figures throughout README.adoc with the
real numbers and a 12-core / 67-advertised / 100+ implementations
framing that tells a new user what they will actually find at the
`/api/provers` endpoint.

Add docs/SUPPORTED_PROVERS.md as the source of truth for the 12-prover
core set: required external binary per prover, install hints, a
working `curl` quickstart against /api/prove, and instructions for
surfacing additional backends through the API.

Add a "Prove your first goal" subsection to README pointing at the new
prove.html UI and the docs page so a new user can go from clone to
verified proof in a few commands.
@hyperpolymath
hyperpolymath enabled auto-merge (squash) May 23, 2026 21:33
@github-actions

github-actions Bot commented May 23, 2026

Copy link
Copy Markdown

🔍 Hypatia Security Scan

Findings: 143 issues detected

Severity Count
🔴 Critical 0
🟠 High 68
🟡 Medium 75
View findings 
[
  {
    "reason": "Issue in quality.yml",
    "type": "missing_workflow",
    "file": "quality.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Issue in security-policy.yml",
    "type": "missing_workflow",
    "file": "security-policy.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Workflow executes remote script directly (curl/wget piped to shell). Download, verify checksum/signature, then execute.",
    "type": "download_then_run",
    "file": "mirror.yml",
    "action": "verify_download_integrity",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "User-defined axiom -- not verified by Lean kernel (1 occurrences, CWE-704)",
    "type": "lean_axiom",
    "file": "/home/runner/work/echidna/echidna/verification/proofs/lean4/IntegrityVerification.lean",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  },
  {
    "reason": "User-defined axiom -- not verified by Lean kernel (1 occurrences, CWE-704)",
    "type": "lean_axiom",
    "file": "/home/runner/work/echidna/echidna/verification/proofs/lean4/ConfidenceLattice.lean",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  },
  {
    "reason": "User-defined axiom -- not verified by Lean kernel (1 occurrences, CWE-704)",
    "type": "lean_axiom",
    "file": "/home/runner/work/echidna/echidna/proofs/lean/mvp_basic.lean",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  },
  {
    "reason": "User-defined axiom -- not verified by Lean kernel (1 occurrences, CWE-704)",
    "type": "lean_axiom",
    "file": "/home/runner/work/echidna/echidna/proofs/lean/Propositional.lean",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  },
  {
    "reason": "Nickel file missing SPDX-License-Identifier header (1 occurrences, CWE-1104)",
    "type": "ncl_missing_spdx",
    "file": "/home/runner/work/echidna/echidna/configs/config.ncl",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  },
  {
    "reason": "expect() in hot path (1 occurrences, CWE-754)",
    "type": "expect_in_hot_path",
    "file": "/home/runner/work/echidna/echidna/src/interfaces/graphql/resolvers.rs",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  },
  {
    "reason": "unwrap() without prior check -- DoS via panic (1 occurrences, CWE-754)",
    "type": "unwrap_without_check",
    "file": "/home/runner/work/echidna/echidna/src/interfaces/graphql/schema.rs",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "high"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence

@claude
chore: lint/format gate clean + expand panic-attack coverage
d14839b 
Brings the tree to `cargo fmt --check` + `cargo clippy -- -D warnings`
clean (the JUST_AND_MUST_FRAMEWORK gate) and adds two new
`tests/panic_attack_props.rs` modules so the proptest harness covers
surfaces exercised by the live REST API.

Lint/format pass:

- Migrate four `rand::Rng::gen_range` / `gen` call sites to the
  non-deprecated `random_range` / `random` API
  (`src/rust/agent/swarm.rs:250,259`,
  `src/rust/learning/design_search.rs:159,173`).
- `cargo clippy --fix` applied 26 `unnecessary_lazy_evaluations`
  suggestions across swarm.rs, graphics.rs, dedukti.rs, client.rs,
  embeddings.rs, graph.rs, design_search.rs, agda.rs, dafny.rs,
  server.rs, suggest/extractor.rs, and vcl_ut.rs.
- `cargo fmt` over the whole tree.

Net: `cargo clippy --lib --no-deps -- -D warnings` exits 0;
`cargo fmt --check` exits 0; `cargo test --lib` still passes
1059/1059 (2 ignored).

Panic-attack expansion (`tests/panic_attack_props.rs`):

- New `metamath_parser_props` module — three properties feeding
  bounded-length arbitrary ASCII, arbitrary bytes, and keyword-heavy
  Metamath-like inputs through `MetamathBackend::parse_string`. The
  parser is the only no-binary prover surface, so this is the only
  way to fuzz the live REST `/api/prove` path in-process. Pin the
  weaker no-panic invariant (Ok-or-Err, never panic) — an empty-state
  parser bug discovered during the API sweep is recorded for separate
  follow-up.
- New `prover_kind_props` module — three properties asserting
  serde JSON round-trip stability, `tier()` ∈ 1..=10, and
  `complexity()` ∈ 1..=5 across every variant in
  `ProverKind::all()`; plus a unit test pinning
  `all_core() ⊆ all()`. The serde round-trip is on every REST
  request path, so a regression here would break the API surface.

Test-suite total: 1467 passing across all targets (20 ignored).
@github-actions

github-actions Bot commented May 23, 2026

Copy link
Copy Markdown

🔍 Hypatia Security Scan

Findings: 152 issues detected

Severity Count
🔴 Critical 9
🟠 High 68
🟡 Medium 75

⚠️ Action Required: Critical security issues found!

View findings 
[
  {
    "reason": "Issue in quality.yml",
    "type": "missing_workflow",
    "file": "quality.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Issue in security-policy.yml",
    "type": "missing_workflow",
    "file": "security-policy.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Workflow executes remote script directly (curl/wget piped to shell). Download, verify checksum/signature, then execute.",
    "type": "download_then_run",
    "file": "mirror.yml",
    "action": "verify_download_integrity",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "User-defined axiom -- not verified by Lean kernel (1 occurrences, CWE-704)",
    "type": "lean_axiom",
    "file": "/home/runner/work/echidna/echidna/verification/proofs/lean4/IntegrityVerification.lean",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  },
  {
    "reason": "User-defined axiom -- not verified by Lean kernel (1 occurrences, CWE-704)",
    "type": "lean_axiom",
    "file": "/home/runner/work/echidna/echidna/verification/proofs/lean4/ConfidenceLattice.lean",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  },
  {
    "reason": "User-defined axiom -- not verified by Lean kernel (1 occurrences, CWE-704)",
    "type": "lean_axiom",
    "file": "/home/runner/work/echidna/echidna/proofs/lean/mvp_basic.lean",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  },
  {
    "reason": "User-defined axiom -- not verified by Lean kernel (1 occurrences, CWE-704)",
    "type": "lean_axiom",
    "file": "/home/runner/work/echidna/echidna/proofs/lean/Propositional.lean",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  },
  {
    "reason": "Nickel file missing SPDX-License-Identifier header (1 occurrences, CWE-1104)",
    "type": "ncl_missing_spdx",
    "file": "/home/runner/work/echidna/echidna/configs/config.ncl",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  },
  {
    "reason": "expect() in hot path (1 occurrences, CWE-754)",
    "type": "expect_in_hot_path",
    "file": "/home/runner/work/echidna/echidna/src/interfaces/graphql/resolvers.rs",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  },
  {
    "reason": "unwrap() without prior check -- DoS via panic (1 occurrences, CWE-754)",
    "type": "unwrap_without_check",
    "file": "/home/runner/work/echidna/echidna/src/interfaces/graphql/schema.rs",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "high"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence

@claude
fix(server): unstale /.well-known/groove + correct prover counts in docs
5d3a8d2 
Earlier corrected count (12 core / 79 advertised) used a stale awk
of `ProverKind::all()` that missed multi-line entries; the runtime
`ProverKind::all().len()` is 79 (verified via `echidna list-provers`
which prints "Total: 79 provers"). Update the README badge, the
README narrative, and `docs/SUPPORTED_PROVERS.md` to match. The
"further 55" line under the API description was a derived figure
from the wrong total — corrected to 67 (= 79 − 12).

`/.well-known/groove` was triple-stale:

  - "Neurosymbolic theorem proving with 48 prover backends"
    (advertised 48; real numbers are 12 core / 79 advertised)
  - `endpoint: /api/v1/prove` — that route does not exist; the live
    handler is `/api/prove`
  - `endpoints.api`/`endpoints.health` hard-coded to port 9000
    (the server defaults to 8081 and the values were also tied
    to a host the daemon does not know)

Replace the manifest with values computed from
`ProverKind::all_core().len()` / `all().len()` so the description
cannot drift, point the capability endpoint at the real
`/api/prove`, and list the live REST routes by relative path
(provers, prove, verify, health). Verified via
`curl /.well-known/groove`: description now reads
"12 core / 79 advertised prover backends".
@github-actions

github-actions Bot commented May 23, 2026

Copy link
Copy Markdown

🔍 Hypatia Security Scan

Findings: 152 issues detected

Severity Count
🔴 Critical 9
🟠 High 68
🟡 Medium 75

⚠️ Action Required: Critical security issues found!

View findings 
[
  {
    "reason": "Issue in quality.yml",
    "type": "missing_workflow",
    "file": "quality.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Issue in security-policy.yml",
    "type": "missing_workflow",
    "file": "security-policy.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Workflow executes remote script directly (curl/wget piped to shell). Download, verify checksum/signature, then execute.",
    "type": "download_then_run",
    "file": "mirror.yml",
    "action": "verify_download_integrity",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "User-defined axiom -- not verified by Lean kernel (1 occurrences, CWE-704)",
    "type": "lean_axiom",
    "file": "/home/runner/work/echidna/echidna/verification/proofs/lean4/IntegrityVerification.lean",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  },
  {
    "reason": "User-defined axiom -- not verified by Lean kernel (1 occurrences, CWE-704)",
    "type": "lean_axiom",
    "file": "/home/runner/work/echidna/echidna/verification/proofs/lean4/ConfidenceLattice.lean",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  },
  {
    "reason": "User-defined axiom -- not verified by Lean kernel (1 occurrences, CWE-704)",
    "type": "lean_axiom",
    "file": "/home/runner/work/echidna/echidna/proofs/lean/mvp_basic.lean",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  },
  {
    "reason": "User-defined axiom -- not verified by Lean kernel (1 occurrences, CWE-704)",
    "type": "lean_axiom",
    "file": "/home/runner/work/echidna/echidna/proofs/lean/Propositional.lean",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  },
  {
    "reason": "Nickel file missing SPDX-License-Identifier header (1 occurrences, CWE-1104)",
    "type": "ncl_missing_spdx",
    "file": "/home/runner/work/echidna/echidna/configs/config.ncl",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  },
  {
    "reason": "expect() in hot path (1 occurrences, CWE-754)",
    "type": "expect_in_hot_path",
    "file": "/home/runner/work/echidna/echidna/src/interfaces/graphql/resolvers.rs",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  },
  {
    "reason": "unwrap() without prior check -- DoS via panic (1 occurrences, CWE-754)",
    "type": "unwrap_without_check",
    "file": "/home/runner/work/echidna/echidna/src/interfaces/graphql/schema.rs",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "high"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence

@claude
fix: unblock PR #100 — clippy --all-targets and verisim-feature build
2c6bd12 
PR #100 was blocked by two required-but-failing CI checks. Both come
from gates I missed in the earlier sweep, neither from a textual
merge conflict (the branch fast-forwards into main cleanly).

**Test Suite** failed on `cargo clippy --all-targets -- -D warnings`.
The earlier lint pass only ran against `--lib`, so two
`manual RangeInclusive::contains` warnings on my new
`prop_tier_in_bounds` / `prop_complexity_in_bounds` properties in
`tests/panic_attack_props.rs:475,484` survived. Rewrite the `x >= lo
&& x <= hi` predicates as `(lo..=hi).contains(&x)`.

**Minimum Supported Rust Version** failed on `cargo check
--all-features`. The original `corpus/octad.rs` LowerHex fix didn't
cover three more `format!("{:x}", ...)` sites that only compile in
when the `verisim` feature is on (see workflow `rust-ci.yml:216` —
the MSRV job uses `--all-features`):

  - `src/rust/proof_encoding.rs:55,65,75` — three identity-hash
    formatters (`proof_identity`, `goal_identity`,
    `session_identity`)
  - `src/rust/verification/proof.rs:55` — Sha256-digest formatter
  - `src/rust/verisim_bridge.rs:979` — same pattern

Promote the existing `to_hex` helper in `src/rust/corpus/octad.rs`
to `pub(crate)` (it was already private and Self-contained — keeps
the dependency direction clean since `corpus` is unconditionally
compiled) and route the five extra call sites through it.

Verification: `cargo fmt --check`, `cargo clippy --all-targets
--no-deps -- -D warnings`, and `cargo check --all-features` all
exit 0. `cargo test --lib` still 1059/1059 (2 ignored);
`cargo test --test panic_attack_props` still 20/20.

Out of scope (pre-existing or environmental, not caused by this PR):
the `Validate A2ML manifests`, `Validate K9 contracts`, `Julia
Integration`, and `T1 / <live-solver>` failures. The A2ML/K9
validators flag missing identity/version/signature fields in files
this PR does not touch; the Julia and live-solver jobs need
toolchains/binaries not provided in the runner. These need their
own follow-ups.
@github-actions

github-actions Bot commented May 23, 2026

Copy link
Copy Markdown

🔍 Hypatia Security Scan

Findings: 241 issues detected

Severity Count
🔴 Critical 9
🟠 High 117
🟡 Medium 115

⚠️ Action Required: Critical security issues found!

View findings 
[
  {
    "reason": "Issue in quality.yml",
    "type": "missing_workflow",
    "file": "quality.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Issue in security-policy.yml",
    "type": "missing_workflow",
    "file": "security-policy.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Workflow executes remote script directly (curl/wget piped to shell). Download, verify checksum/signature, then execute.",
    "type": "download_then_run",
    "file": "mirror.yml",
    "action": "verify_download_integrity",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "User-defined axiom -- not verified by Lean kernel (1 occurrences, CWE-704)",
    "type": "lean_axiom",
    "file": "/home/runner/work/echidna/echidna/verification/proofs/lean4/IntegrityVerification.lean",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  },
  {
    "reason": "User-defined axiom -- not verified by Lean kernel (1 occurrences, CWE-704)",
    "type": "lean_axiom",
    "file": "/home/runner/work/echidna/echidna/verification/proofs/lean4/ConfidenceLattice.lean",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  },
  {
    "reason": "User-defined axiom -- not verified by Lean kernel (1 occurrences, CWE-704)",
    "type": "lean_axiom",
    "file": "/home/runner/work/echidna/echidna/proofs/lean/mvp_basic.lean",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  },
  {
    "reason": "User-defined axiom -- not verified by Lean kernel (1 occurrences, CWE-704)",
    "type": "lean_axiom",
    "file": "/home/runner/work/echidna/echidna/proofs/lean/Propositional.lean",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  },
  {
    "reason": "Nickel file missing SPDX-License-Identifier header (1 occurrences, CWE-1104)",
    "type": "ncl_missing_spdx",
    "file": "/home/runner/work/echidna/echidna/configs/config.ncl",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  },
  {
    "reason": "expect() in hot path (1 occurrences, CWE-754)",
    "type": "expect_in_hot_path",
    "file": "/home/runner/work/echidna/echidna/src/interfaces/graphql/resolvers.rs",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  },
  {
    "reason": "unwrap() without prior check -- DoS via panic (1 occurrences, CWE-754)",
    "type": "unwrap_without_check",
    "file": "/home/runner/work/echidna/echidna/src/interfaces/graphql/schema.rs",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "high"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence

@claude
fix(ci): unblock Test Suite, MSRV, K9, and A2ML gates
28e6805 
Round 2 of CI-failure triage on PR #100. The first round only fixed
`cargo clippy --lib --no-deps`; the real Test Suite job runs
`--all-targets --all-features` (workflow: `rust-ci.yml:60`) which
exposes feature-gated lints my local check missed. MSRV (rust 1.85,
`cargo check --all-features`) failed on transitive-dep MSRV drift
*and* on one use of a 1.87-stabilised method. K9 and A2ML manifest
validators are external GitHub actions that text-scan files for
required fields; the failing files lack them in the right form.

**Test Suite** (`cargo clippy --all-targets --all-features -- -D warnings`)

  Three more `unwrap_or_else(|| 0)` → `unwrap_or(0)` sites, all
  behind the `verisim` feature so the earlier `clippy --fix` pass
  did not touch them:

    - `src/rust/vcl_ut.rs:809`
    - `src/rust/verisim_bridge.rs:992,993`

**MSRV** (`cargo check --all-features` on rust 1.85)

  Two independent regressions, both pre-existing on `main`:

  1. **Transitive dep drift.** Latest `home@0.5.12`, `icu_*@2.2.0`,
     `idna_adapter@1.2.1` bumped their MSRVs above 1.85. Pinned
     compatible versions in `Cargo.lock` via `cargo update --precise`:

       - `home`           0.5.12 → 0.5.11   (MSRV 1.88 → none)
       - `idna_adapter`   1.2.1  → 1.2.0    (drags icu down to 2.1)
       - `icu_collections`, `icu_normalizer`, `icu_normalizer_data`,
         `icu_properties`, `icu_properties_data`             2.2.x → 2.1.x
       - `zerovec`, `zerovec-derive`                         0.11 → 0.10

  2. **`u64::is_multiple_of`** at `coprocessor/math.rs:387` —
     stabilised in 1.87, doesn't compile on 1.85. Rewrite as
     `n % 2 == 0` and `#[allow(clippy::manual_is_multiple_of)]`
     to avoid the stable-clippy catch-22 (stable wants the method,
     1.85 cannot have it). Comment explains the MSRV constraint
     so a future bump removes the workaround.

**Validate A2ML manifests** (`hyperpolymath/a2ml-validate-action`)

  Six files were missing structured identity / version / SPDX
  fields. The validator text-scans TOML keys; comment-style
  `# identity:` did not satisfy it.

    - `training_data/{tactics,stats,proof_states}_*.a2ml` ×5 —
      added `name = "..."` and `project = "echidna"` inside the
      existing `[metadata]` block.
    - `audits/assail-classifications.a2ml` — Lisp-syntax file with
      no TOML preamble. Added a `[metadata]` block (name / project /
      version / schema_version) before the Lisp body and converted
      the leading `;` comments to `#` so the preamble is contiguous.
    - `.machine_readable/6a2/ANCHOR.a2ml` — missing SPDX in the
      first 10 lines. Added `# SPDX-License-Identifier: MPL-2.0`
      as line 1.

**Validate K9 contracts** (`hyperpolymath/k9-validate-action`)

  The validator inspects the literal `pedigree = { ... }` block;
  it does not resolve Nickel `let` bindings.

    - `container/deploy.k9.ncl` — the pedigree had its identity
      fields inside a `component_pedigree` let-binding the
      validator cannot follow. Duplicate `name`, `version`,
      `schema_version`, `security_level`, `signature_required` at
      the top of the pedigree record (the existing nested
      `metadata`/`security` keys are preserved for the runtime
      consumer). Comment explains the duplication.
    - `.machine_readable/contractiles/bust/bust.k9.ncl` — added
      `signature_required = true` to the Hunt-tier security block.
      Comment notes that signature enforcement lives at the
      trident-runner layer, not in-band.

**Local gate** (every command CI runs on the rust side)

    cargo fmt --check                                       → 0
    cargo clippy --all-targets --all-features -D warnings   → 0
    cargo +1.85 check --all-features                        → 0
    cargo test --lib --features verisim                     → 1092/1092 pass
    cargo test --test integration_tests --features verisim  →   38/38   pass
    cargo test --test panic_attack_props                    →   20/20   pass

**Still out of scope** (separate workstreams):

  - `Julia Integration` — needs Julia toolchain in runner
  - `Code Coverage` — `cargo tarpaulin` issue, will re-investigate
    after this round
  - `T2/T3/T4` provers — skipped by matrix design
  - `PR (address)` and `MVP Smoke` — will investigate next round
    if still failing after this push
@github-actions

github-actions Bot commented May 24, 2026

Copy link
Copy Markdown

🔍 Hypatia Security Scan

Findings: 251 issues detected

Severity Count
🔴 Critical 10
🟠 High 120
🟡 Medium 121

⚠️ Action Required: Critical security issues found!

View findings 
[
  {
    "reason": "Issue in quality.yml",
    "type": "missing_workflow",
    "file": "quality.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Issue in security-policy.yml",
    "type": "missing_workflow",
    "file": "security-policy.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Workflow executes remote script directly (curl/wget piped to shell). Download, verify checksum/signature, then execute.",
    "type": "download_then_run",
    "file": "mirror.yml",
    "action": "verify_download_integrity",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "User-defined axiom -- not verified by Lean kernel (1 occurrences, CWE-704)",
    "type": "lean_axiom",
    "file": "/home/runner/work/echidna/echidna/verification/proofs/lean4/IntegrityVerification.lean",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  },
  {
    "reason": "User-defined axiom -- not verified by Lean kernel (1 occurrences, CWE-704)",
    "type": "lean_axiom",
    "file": "/home/runner/work/echidna/echidna/verification/proofs/lean4/ConfidenceLattice.lean",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  },
  {
    "reason": "User-defined axiom -- not verified by Lean kernel (1 occurrences, CWE-704)",
    "type": "lean_axiom",
    "file": "/home/runner/work/echidna/echidna/proofs/lean/mvp_basic.lean",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  },
  {
    "reason": "User-defined axiom -- not verified by Lean kernel (1 occurrences, CWE-704)",
    "type": "lean_axiom",
    "file": "/home/runner/work/echidna/echidna/proofs/lean/Propositional.lean",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  },
  {
    "reason": "Nickel file missing SPDX-License-Identifier header (1 occurrences, CWE-1104)",
    "type": "ncl_missing_spdx",
    "file": "/home/runner/work/echidna/echidna/configs/config.ncl",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  },
  {
    "reason": "expect() in hot path (1 occurrences, CWE-754)",
    "type": "expect_in_hot_path",
    "file": "/home/runner/work/echidna/echidna/src/interfaces/graphql/resolvers.rs",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  },
  {
    "reason": "unwrap() without prior check -- DoS via panic (1 occurrences, CWE-754)",
    "type": "unwrap_without_check",
    "file": "/home/runner/work/echidna/echidna/src/interfaces/graphql/schema.rs",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "high"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence

@claude
fix(k9): inline pedigree fields in deploy.k9.ncl toplevel record
436532e 
Round 3 of CI triage. The previous fix added the K9 identity fields
(name / version / security_level / signature_required) to the
`component_pedigree` Nickel let-binding, but the K9 validator text-
scans the literal `pedigree = { ... }` block at the toplevel of the
file — it does not resolve Nickel let-bindings. Confirmed by the
validator continuing to report the same three missing fields on
`./container/deploy.k9.ncl#L1` after the previous round:

  - Pedigree block missing 'name' field
  - No security level (leash/security_level) found in pedigree block
  - Pedigree block missing 'version' or 'schema_version' field

Restructure the toplevel record so that `pedigree = { ... }` is an
inline record literal containing the identity fields directly, with
the substructures (metadata, target, security, validation, recipes)
delegated to `component_pedigree`. The runtime consumer sees the
same resolved value as before; only the textual layout changes.

Comment in the file explains the validator's literal-text-scan
behaviour so a future restructure doesn't regress this.

The bust.k9.ncl fix from the previous round held: that file is no
longer in the validator's error list.
@github-actions

github-actions Bot commented May 24, 2026

Copy link
Copy Markdown

🔍 Hypatia Security Scan

Findings: 251 issues detected

Severity Count
🔴 Critical 10
🟠 High 120
🟡 Medium 121

⚠️ Action Required: Critical security issues found!

View findings 
[
  {
    "reason": "Issue in quality.yml",
    "type": "missing_workflow",
    "file": "quality.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Issue in security-policy.yml",
    "type": "missing_workflow",
    "file": "security-policy.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Workflow executes remote script directly (curl/wget piped to shell). Download, verify checksum/signature, then execute.",
    "type": "download_then_run",
    "file": "mirror.yml",
    "action": "verify_download_integrity",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "User-defined axiom -- not verified by Lean kernel (1 occurrences, CWE-704)",
    "type": "lean_axiom",
    "file": "/home/runner/work/echidna/echidna/verification/proofs/lean4/IntegrityVerification.lean",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  },
  {
    "reason": "User-defined axiom -- not verified by Lean kernel (1 occurrences, CWE-704)",
    "type": "lean_axiom",
    "file": "/home/runner/work/echidna/echidna/verification/proofs/lean4/ConfidenceLattice.lean",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  },
  {
    "reason": "User-defined axiom -- not verified by Lean kernel (1 occurrences, CWE-704)",
    "type": "lean_axiom",
    "file": "/home/runner/work/echidna/echidna/proofs/lean/mvp_basic.lean",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  },
  {
    "reason": "User-defined axiom -- not verified by Lean kernel (1 occurrences, CWE-704)",
    "type": "lean_axiom",
    "file": "/home/runner/work/echidna/echidna/proofs/lean/Propositional.lean",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  },
  {
    "reason": "Nickel file missing SPDX-License-Identifier header (1 occurrences, CWE-1104)",
    "type": "ncl_missing_spdx",
    "file": "/home/runner/work/echidna/echidna/configs/config.ncl",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  },
  {
    "reason": "expect() in hot path (1 occurrences, CWE-754)",
    "type": "expect_in_hot_path",
    "file": "/home/runner/work/echidna/echidna/src/interfaces/graphql/resolvers.rs",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  },
  {
    "reason": "unwrap() without prior check -- DoS via panic (1 occurrences, CWE-754)",
    "type": "unwrap_without_check",
    "file": "/home/runner/work/echidna/echidna/src/interfaces/graphql/schema.rs",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "high"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence

@hyperpolymath
hyperpolymath merged commit 946541f into main May 24, 2026
41 of 45 checks passed
@hyperpolymath
hyperpolymath deleted the claude/determined-archimedes-Sgffi branch May 24, 2026 04:56
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@hyperpolymath @claude